As computer programs have become increasingly complex, the challenges of developing reliable software have become apparent. Modern software applications can contain millions of lines of code written by many different developers, and each developer may have different programming skills and styles. In addition, because many large applications are developed over a period of several years, the team of developers that begins work on an application may be different than the team that completes the project. Therefore, the original authors of software code may not be available to error-check and revise the code during the development process. For all of these reasons, despite recent improvements in software engineering techniques, debugging of software applications remains a daunting task.
The basic concepts of software engineering are familiar to those skilled in the art. For example, FIG. 1 shows a technique 100 for developing a computer program according to the prior art. First, at 110, a program is created/edited by one or more developers. Then, at 120, the program is debugged (e.g., using a debugging tool). At 130, if the program contains bugs to be fixed, or if other revisions are desired, the editing/debugging cycle continues. After debugging and editing, the source code is compiled into executable code. FIG. 2 shows a block diagram of a system for compiling source code according to the prior art. A compiler 200 compiles source code written in a high-level language in source files 205 into executable code 210 for execution on a computer. The executable code 210 can be hardware-specific or generic to multiple hardware platforms. The compiler 200 can use, for example, lexical analysis, syntax analysis, code generation and code optimization to translate the source code into executable code. In addition, many compilers have debugging capabilities for detecting and describing errors at compile time.
The size and complexity of most commercially valuable software applications have made detecting every programming error in such applications nearly impossible. To help manage software development and debugging tasks and to facilitate extensibility of large applications, software engineers have developed various techniques of analyzing, describing and/or documenting the behavior of programs to increase the number of bugs that can be found before a software product is sold or used. Such techniques include instrumentation, in which additional error-checking code is added to a program, and the writing of program specifications to describe the behavior of programs. Program specifications can be written in specially-designed specification languages, which follow their own syntactic rules for describing program behavior. However, specification languages are often complex, and writing a specification for a complex program can be similar in terms of programmer burden to re-writing the program in a new language.
As programs become larger and more complex, it becomes increasingly beneficial to split programs into modules whose behavior can be understood in isolation by programmers and verification tools. Annotations can be used to describe behavior of program modules (e.g., functions) and programs as a whole (e.g., when annotated modules are analyzed in combination) by making assertions about program states. Although annotations on source code help programmers and verification tools interpret the behavior of programs and program modules, the overhead of adding annotations to source code (particularly in the case of previously developed, or “legacy,” source code) has limited their use. In addition, the set of properties that are important for analyzing program behavior varies widely across programs, as do the ways in which data flows within programs. For instance, locking behavior may be important for multi-threaded programs but not for sequential programs, while buffer size information may be important for programs written in C or C++ but not for programs written in Java or C#.